A, B, C:Realizer. R-Feasible(C)  A  C  B  C  A || B 

latex

Definitions

{T}, SQType(T), , ff, tt, Rnone?(x1), if b then t else f fi , Y, Rplus-right(x1), Rplus-left(x1), P & Q, Rplus?(x1), A || B, i  j , False, A, A  B, t  T, P  Q, x:A. B(x), R-Feasible(R), P  Q, Unit, , A  B, P  Q, Dec(P), , ,

Lemmas

R-compat-self, R-sub-self, bool sq, bool cases, R-compat wf, Rnone wf, R-compat-symmetry, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, R-compat-none, Rnone-implies, Rnone? wf, Rplus-right wf, Rplus-left wf, Rplus-implies, R-size-decreases, Rplus? wf, decidable assert, ge wf, nat properties, le wf, es realizer wf, R-Feasible wf, R-sub wf, nat plus wf, R-size wf, nat wf